PRISM

Benchmark
Model:herman v.1 (DTMC)
Parameter(s)N = 15
Property:steps (exp-reward)
Invocation (default)
./fix-syntax ./prism -javamaxmem 11g -cuddmaxmem 4g -ii -e 5e-2 -heuristic speed -ddextraactionvars 100 -maxiters 1000000 herman.15.prism herman.props --property steps
Execution
Walltime:10.43846583366394s
Return code:0
Relative Error:0.0254963257750091
Log
PRISM
=====

Version: 4.5.dev
Date: Sat Mar 14 12:15:20 UTC 2020
Hostname: e72bdd194fc5
Memory limits: cudd=4g, java(heap)=11g
Command line: prism -javamaxmem 11g -cuddmaxmem 4g -ii -e 5e-2 -heuristic speed -ddextraactionvars 100 -maxiters 1000000 herman.15.prism herman.props --property steps

Parsing model file "herman.15.prism"...

Type:        DTMC
Modules:     process1 process2 process3 process4 process5 process6 process7 process8 process9 process10 process11 process12 process13 process14 process15 
Variables:   x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 

Parsing properties file "herman.props"...

1 property:
(1) "steps": filter(max, R=? [ F "stable" ], "init")

---------------------------------------------------------------------

Model checking: "steps": filter(max, R=? [ F "stable" ], "init")

Warning: Switching to sparse engine and (backwards) Gauss Seidel (default for heuristic=speed).

Building model...

Computing reachable states...

Reachability (BFS): 1 iterations in 0.00 seconds (average 0.000000, setup 0.00)

Time for model construction: 0.025 seconds.

Type:        DTMC
States:      32768 (32768 initial)
Transitions: 14348908

Transition matrix: 810 nodes (9 terminal), 14348908 minterms, vars: 15r/15c

Prob0: 6 iterations in 0.03 seconds (average 0.005333, setup 0.00)

Prob1: 1 iterations in 0.00 seconds (average 0.000000, setup 0.00)

goal = 30, inf = 0, maybe = 32738
Time for computing an upper bound for expected reward: 0.889 seconds.
Upper bound for expectation (variant 2): 3523713.2050052434

Computing remaining rewards...
Engine: Sparse

Building sparse matrix... [n=32768, nnz=14348846, compact] [54.9 MB]
Creating vector for diagonals... [dist=2, compact] [64.0 KB]
Creating vector for RHS... [dist=2, compact] [64.0 KB]
Allocating iteration vectors... [ 2 x 256.0 KB]
TOTAL: [55.5 MB]

Starting iterations...
Iteration 115: max relative diff=0.876783, 5.03 sec so far
Max relative diff between upper and lower bound on convergence: 0.0485192
Backwards Gauss-Seidel (interval iteration): 171 iterations in 8.68 seconds (average 0.043813, setup 1.18)
Maximum finite value in solution vector at end of interval iteration: 34.18321085916697

Maximum value over states satisfying filter: 34.18321085916697

There are 70 states with (approximately) this value.
The first 10 states are displayed below. To view them all, enable verbose mode or use a print filter.
5285:(0,0,1,0,1,0,0,1,0,1,0,0,1,0,1)
5293:(0,0,1,0,1,0,0,1,0,1,0,1,1,0,1)
5301:(0,0,1,0,1,0,0,1,0,1,1,0,1,0,1)
5541:(0,0,1,0,1,0,1,1,0,1,0,0,1,0,1)
5549:(0,0,1,0,1,0,1,1,0,1,0,1,1,0,1)
5797:(0,0,1,0,1,1,0,1,0,1,0,0,1,0,1)
5813:(0,0,1,0,1,1,0,1,0,1,1,0,1,0,1)
9513:(0,1,0,0,1,0,1,0,0,1,0,1,0,0,1)
9515:(0,1,0,0,1,0,1,0,0,1,0,1,0,1,1)
9517:(0,1,0,0,1,0,1,0,0,1,0,1,1,0,1)

Time for model checking: 9.618 seconds.

Result: 34.18321085916697 (maximum value over states satisfying filter)


Overall running time: 10.257 seconds.

---------------------------------------------------------------------

Note: There was 1 warning during computation.